FDL - Nuprl Lemma : conditional-apply

Nuprl Lemma : conditional-apply

T, V:Type, A, B:(T

), dcd_A:(t:T

Dec(A(t))), f:({t:T| A(t)}

V), g:({t:T| B(t)}

V),

t:{t:T| (A(t))

(B(t))} .
((A(t))

([A? f : g](t) = f(t))) & ((

(A(t)))

([A? f : g](t) = g(t)))

Definitions f(a), left + right, P Q, {x:A| B(x)} , t T, x:AB(x), x:A. B(x), False, P Q, A, Dec(P), s = t, , if p:P then A(p) else B fi , Type, <a, b>, P & Q, [P? f : g]